Inference at * 1 1 4 2 1 2 
Iof proof for Lemma gen hyp tp:

.....wf..... NILNIL

1. A : Type
2. e : A
3. H : AType
4. x : A
5. e = x
6. H(e)
7. A  Type
8. e  A
9. x:A. (e = x)  Type
  z1:{x:A| e = x} . H(z1)  Type 

latex

 by (%L:wf% 
% if hyp i is not a declaration, then quantifier type 

% ifwill already be on the lhs of the >> % 
\p. 
if is_visible_var (var_of_hyp (
ifget_int_arg `i` p + 2) p) then 
((At (get_term_arg `UA` p) (D 0)) 
(CollapseTHENA (
(CMemCD THENL [SoftNthHyp (-3);((BackThruHyp (-2)) 
(CollapseTHEN (NthDecl (-1)))])) p 
else 

elseId p) 

latex

el1: 

el1: 10. z1 : {x:A| e = x} 
el1:   H(z1)  Type
el.

Definitions

x:A. B(x), t  T